T:Type, L:(T List). ||rev(L)|| ~ ||L|| 

latex

Definitions	n+m, as @ bs, ||as||, #$n, x:A. B(x), s ~ t, x:AB(x), Type, s = t, type List, t  T
Lemmas	length-append